For the moment, we only generate a precondition with [disjoint]
if a function has two represented arguments of the same type.

TODO:
  1. Extend the generation of the [disjoint] predication for an
     arbitrary number of represented arguments
  2. Check the [modifies] clause in order to generate the correct
     set of [disjoint] preconditions. Example: consider the following
     GOSPEL specification:
       val f : 'a t -> 'a t -> 'a t -> unit
       (*@ f x y z
             modifies x
             requires P
             ensures  Q *)
     where ['a t] is some represented type. For this case, we should
     generate the following WhyML declaration:
       val f (x y z: t 'a) : unit
         requires { disjoint_t x y }
         requires { disjoint_t x z }
         writes   { x }
         requires { P }
         ensures  { Q }
     Let me explain: since argument [x] is listed in [modifies],
     it must be disjoint of any other argument of type ['a t].
     Otherwise, if [x] was not disjoint of [y] or [z], either [y]
     or [z] could be aliased with [x], hence modified by [f]. On
     the other hand, since [y] and [z] are read-only arguments,
     they do not need to be disjoint from each other.